\documentclass[a4paper,10pt]{article}
\usepackage[utf8x]{inputenc}
\usepackage{proof}
\usepackage{multirow}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{array}
\usepackage{textcomp}
\usepackage{amsthm}
\usepackage{macros-short}

\setlength\topmargin{0in}
\setlength\headheight{0in}
\setlength\headsep{0in}
\setlength\textheight{8.7in}
\setlength\textwidth{6.5in}
\setlength\oddsidemargin{0in}
\setlength\evensidemargin{0in}
\setlength\headheight{0pt}
\setlength\headsep{0.0in}

\theoremstyle{plain}% default
\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}[thm]{Lemma}
\newtheorem{prop}[thm]{Proposition}
\newtheorem*{cor}{Corollary}
\newtheorem*{KL}{Klein's Lemma}
\newtheorem{algo}{Algorithm}

\theoremstyle{definition}
\newtheorem{defn}{Definition}[section]
\newtheorem{conj}{Conjecture}[section]
\newtheorem{exmp}{Example}[section]

\theoremstyle{remark}
\newtheorem*{rem}{Remark}
\newtheorem*{note}{Note}
\newtheorem{case}{Case}

%opening
\title{Outline}
%\author{Junkil Park}

\begin{document}

\maketitle

\begin{abstract}
As real-time embedded systems become more complex, resource
partitioning is increasingly used to guaranteed real-time performance.
Recently, several compositional framework of resource partitioning have been proposed
using real-time scheduling theory with various notions of
real-time tasks running under restricted resource supply environment.
However, the real-time scheduling based approaches are limited in
expressibility of resource-demand tasks and also resource supply.
This paper describes a process algebraic framework for reasoning about
resource demand and supply.  The approach is based on the timed
process algebra, ACSR.  In ACSR, real-time tasks are specified by when
they need to consume resource CPU. For resource-supply process, we define ACSR+,
where the complimented resource $\overline{CPU}$ denotes for availability
of CPU for the corresponding demand process.  Using ACSR and ACSR+, we
define a supply-demand relation, (S, P), where the relation is true if
the demand process P can be scheduled under the supply model S.
Finally, we define the notion of compositional schedulability analysis
and show that our framework is compositional.  As an illustration, we
use VERSA, a tool kit for ACSR, to check of truth of supply-demand
relation and compositional schedulability analysis.

\end{abstract}

\section{Introduction}
\subsection{Motivation}

Embedded systems become more complex. Component-based design has been widely accepted. It is required to analyze timing properties in composition of components.

\subsection{Problems}

We use the term \textit{scheduling unit} to mean the basic unit of scheduling and define scheduling unit $S$ as a triple $(W, R, A)$, where $W$  describes the workloads supported unit, $R$ is a resource model that describes the resource allocations available to the scheduling unit, and $A$ is a scheduling algorithm which describes how the workloads share the resources at all times. We consider that \textit{component} $C$ consists of a workload set $W$ and a scheduling algorithm $A$ for $W$, denoted $C(W,A)$. The \textit{real-time interface} $I$ of a component $C(W,A)$ specifies the collective real-time requirements of the component $C$, which $W$ demands under $A$, without revealing the internal information of the component, such as the number of its workloads and its scheduling algorithm. A real-time interface $I$ of component $C(W,A)$ is said to be \textit{schedulable} if scheduling unit $S(W,R,A)$ is schedulable with $R = I$. We address the following two problems:
\begin{itemize}
 \item for a scheduling unit $S(W,R,A)$, the problem is to analyze its schedulability;
 \item for a component $C(W,A)$, the problem is to generate an optimal interface $I$.
\end{itemize}


\subsection{Approach}

For the schedulability problem, we introduce ACSR+ extending ACSR with notion of \textit{resource supply} and \textit{schedulable under}. Given a scheduling unit $S(W, R, A)$, we model $W$ and $A$ as an ordinary ACSR process $D$. We model $R$ as a supply process $S$ with a new syntax of supply description language to be defined in this paper. For schedulability analysis, we check $S \models D$ where $\models$ is a \textit{schedulable under relation} to be defined in this paper. We check $\models$ by reducing it into bisimulation (or deadlock) checking of ACSR.

For the interface generation problem, we assume the interface model is \textit{periodic}\cite{PERIODIC} (or \textit{explicit deadline periodic}). We reduce interface generation problem to schedulability problem. Given a component $C$ and a period of interface $P_0$, the optimal interface is $P(P_0, E_0)$ with the minimum $E_0$ such that $P$ of $C$ is schedulable.

We consider the single processor system, so we assume that there is one resource called $cpu$. For modeling resource demanding, we use a subset of ACSR. We say an ACSR process is a \textit{basic process} if it is defined without the parallel composition operator $\parallel$. We say an ACSR process is a \textit{parallel process} if it is defined in the form of $P_1 \parallel \cdots \parallel P_n$ where $P_i$ is a basic process. We model a periodic task as a basic ACSR process. We model a system model that is a set of tasks running concurrently as a parallel process. For modeling resource supply, we introduce ACSR+. $\overline{cpu}$ represnts granting $cpu$. We model periodic resource model as a ACSR+ process.

We define supply-demand relation. There is a relation between a set of supply traces and a set of demand traces if for every supply trace, there exists a demand trace suppliable. For schedulability analysis, we introduce the notion of k-semideterministic and ASAP for using $cpu$. We refine the supply demand relation according to the notion. In order to check the truth of the refined relation, we translate supply process into ACSR process and use VERSA to analyze it.

We also provide the results on compositionality. 

\subsection{Contribution}
% \begin{itemize}
%  \item We provide process algebraic compositional real-time scheduling framework. We provide a extended process algebra ACSR+ with the supply notion.
%  \item We provide not only periodic task and resource model but also any general ones which can be modeled in ACSR+.
%  \item We provide not only scheduling algorithms RM, EDF but also any one that can be modeled in ACSR+.
% \end{itemize}

\begin{itemize}
 \item We provide a novel process algebra ACSR+ with new notion of resource supply in order to take account of resource supply constraints of real-time systems.
 \item We provide a new method to solve interface generation problem by reducing it to schedulability problem.
 % extends criteria of optimality in interface generation
 \item We provide a process algebraic framework of compositional scheduling which is more general than the existing one. Our framework can handle more realistic system models, and model more general resource supply than \textit{periodic} and \textit{explicit deadline periodic}.
\end{itemize}

\section{Modeling Task Demand (ACSR)}
\subsection{ACSR Syntax and Semantics}
In our framework, we use a subset of ACSR processes \cite{ACSR} to describe demand processes. We focus on single processor system, so assume that there is one serially-reusable resources called $cpu$. Timed actions may require access to the system resource $cpu$. An action consumes one ``tick'' of time and employs a set of resources, each with an integer priority. For example, action $\{(cpu, n)\}$ denotes the use of $cpu$ running at priority level $n \geq 0$. The action $\emptyset$, consuming no resources, represents idling for one time unit. We use $\mathcal{D}_R = \{\emptyset, \{(cpu, n)\} \mid n \geq 0 \}$ to denote the domain of timed actions ranged over by $A$. ACSR processes are described by the following grammar, where we assume a set of process constants each with an associated definition of the kind $C\stackrel{\mathrm{def}}{=}P.$

\begin{eqnarray}
P &::=& A:P \textrm{ $|$ } P + P \textrm{ $|$ } P \parallel P \textrm{ $|$ } C \nonumber \\
A &::=& \emptyset \textrm{ $|$ } \{(cpu,n)\} \nonumber
\end{eqnarray}

We say an ACSR process is a \textit{basic process} if it is defined without the parallel composition operator $\parallel$. We say an ACSR process is a \textit{parallel process} if it is defined in the form of $P_1 \parallel \cdots \parallel P_n$ where $P_i$ is a basic process.

%Steps of
ACSR processes are constructed using the prefix operator. The process $A$:$P$ executes a resource-consuming action during the first time unit and proceeds to $P$. The process $P + Q$ represents nondeterministic choice. $P \parallel Q$ describes the concurrent composition of $P$ and $Q$.

The executions of a process are defined by a timed labeled transition system (timed LTS). A timed LTS, $M$, is defined as $(\mathcal{P},\mathcal{D}_R, \rightarrow , P_0)$, where $\mathcal{P}$ is a set of ACSR processes, ranged over by $P$ and $Q$, $\mathcal{D}$ is a set of actions, and $\rightarrow$ is a labeled transition relation such that $P\stackrel{A}{\longrightarrow} Q$ if process $P$ may perform an instantaneous event or timed action $\alpha$ and then behave as $Q$. $P_0 \in \mathcal{P}$ represents the initial state of the system.

The prioritized transition system is based on \emph{preemption}, which incorporates our treatment of priority. This is based on a transitive, irreflexive, binary relation on actions, $\prec$ called the \emph{preemption relation}. If $A \prec A'$, for two actions $A$ and $A'$, we say that $A$ is \emph{preempted by} $A'$. Given two actions $A$, $A'$, we say that $A \prec A'$ iff $A = \{(cpu,n)\}$, $A' = \{(cpu,m)\}$ and $n<m$. Then, in any process, if there is a choice between executing either $A$ or $A'$, $A'$ will always be executed. We define the prioritized transition system ``$\rightarrow_{\pi}$'', which simply refines ``$\rightarrow$'' to account for preemption. The labeled transition system ``$\rightarrow_{\pi}$'' is defined as follows: $P\stackrel{A}{\longrightarrow}_{\pi} P'$ if and only if (1) $P\stackrel{A}{\longrightarrow} P'$ is an unprioritized transition, and (2) there is no unprioritized transition $P\stackrel{A'}{\longrightarrow} P''$ such that $A \prec A'$ (for more detail see \cite{ACSR}).


%ACSR, like other process algebras, consists of (1) a set of operators and syntactic rules for constructing process; (2) a semantic mapping which assigns meaning or interpretation to processes; (3) a notion of equivalence or partial order between process; and (4) a set of algebraic laws that allows syntactic manipulation of processes. ACSR uses two distinct action types to model computation: time and resource-consuming actions, and instantaneous events.

%ACSR distinguish two types of actions: those which consume time, and those which are instantaneous. Timed actions may require access to system resources, e.g., cpu's, memory, batteries, etc. In contrast, instantaneous actions provide a synchronization mechanism between concurrent processes.

%\textbf{Timed Actions.} A system has a finite set of serially-reusable resources, $\mathcal{R}$. An action consumes one ``tick'' of time and employs a set of resources, each with an integer priority. For example, action $\{(r, p)\}$ denotes the use of some resource $r \in \mathcal{R}$ running at priority level $p$. The action $\emptyset$, consuming no resources, represents idling for one time unit.

%\textbf{Events.} Instantaneous actions, or events, provide process synchronization in ACSR. An event is denoted by a pair $(a, p)$, where $a$ is the label of the event, and $p$ is its priority. Labels represent input and output actions on channels. As in CCS, the special identity label, $\tau$ , arises when two events with input and output on the same channel synchronize. We define $\mathcal{L}$ as the set of all event labels.

%We use $\mathcal{D}_R$ to denote the domain of timed actions ranged over by $A$ and $B$. We use $\mathcal{D}_E$ to denote the domain of events ranged over by $e$ and $f$, and $\mathcal{D} = \mathcal{D}_R \cup \mathcal{D}_E$ to denote the entire domain of actions ranged over by $\alpha$ and $\beta$.

%ACSR processes are described by the following grammar, where we assume a set of process constants each with an associated definition of the kind $C\stackrel{\mathrm{def}}{=}P.$
%\begin{eqnarray}
%P &::=& NIL \textrm{ $|$ } e.P \textrm{ $|$ }  A\textrm{:}P \textrm{ $|$ }  P+P \textrm{ $|$ }  P \parallel P \textrm{ $|$ }  P\backslash F \textrm{ $|$ }  [P]_{I} \textrm{ $|$ }    \nonumber\\
%  &   & P\backslash\backslash I \textrm{ $|$ } P\Delta ^{\alpha} _{t}(P, P, P) \textrm{ $|$ }  C \nonumber
%\end{eqnarray}

%Steps of ACSR processes are constructed using the two prefix operators corresponding to the two types of actions. The process $e.P$ executes the instantaneous event $e$ and proceeds to $P$. The process $A$:$P$ executes a resource-consuming action during the first time unit and proceeds to $P$. The process $P + Q$ represents nondeterministic choice and the process $P \parallel Q$ describes the concurrent composition of $P$ and $Q$. The temporal scope construct, $P\Delta ^{\alpha} _{t}(Q, R, S)$, restricts a process $P$ by a time limit $(t)$. If $P$ completes its execution within this limit an exception, $\alpha$, is thrown, in which case an exception handler $(Q)$ is executed. If not, control is passed to a timeout process $(R)$. In any case, $P$ can be interrupted by a step of an interrupt process $(S)$. Other static operators of ACSR allow us to hide the identity of certain resources $(P\backslash\backslash I)$, reserve the use of a resource for a given process $([P]_{I})$, and force synchronization between processes by restricting certain events $(P\backslash F)$.

%The executions of a process are defined by a timed labeled transition system (timed LTS). A timed LTS, $M$, is defined as $(\mathcal{P},\mathcal{D}, \rightarrow , P_0)$, where $\mathcal{P}$ is a set of ACSR processes, ranged over by $P$ and $Q$, $\mathcal{D}$ is a set of actions, and $\rightarrow$ is a labeled transition relation such that $P\stackrel{\alpha}{\longrightarrow} Q$ if process $P$ may perform an instantaneous event or timed action $\alpha$ and then behave as $Q$. $P_0 \in \mathcal{P}$ represents the initial state of the system.

%The prioritized transition system is based on \emph{preemption}, which incorporates our treatment of priority. This is based on a transitive, irreflexive, binary relation on actions, $\prec$ called the \emph{preemption relation}. If $\alpha \prec \beta$, for two actions $\alpha$ and $\beta$, we say that $\alpha$ is \emph{preempted by} $\beta$. Then, in any process, if there is a choice between executing either $\alpha$ or $\beta$, $\beta$ will always be executed. We define the prioritized transition system ``$\rightarrow_{\pi}$'', which simply refines ``$\rightarrow$'' to account for preemption. The labeled transition system ``$\rightarrow_{\pi}$'' is defined as follows: $P\stackrel{\alpha}{\longrightarrow}_{\pi} P'$ if and only if (1) $P\stackrel{\alpha}{\longrightarrow} P'$ is an unprioritized transition, and (2) there is no unprioritized transition $P\stackrel{\beta}{\longrightarrow} P''$ such that $\alpha \prec \beta$. We refer to [?] for the precise definition of $\prec$ and semantics of ACSR operators.

\subsection{Specifying System Models in ACSR}

A system model consists of a workload model and a scheduling algorithm. ACSR can capture following characteristics of system models. This subsection will be refined later.

\noindent(1) A task in a workload can be
\begin{itemize}
 \item dependant or independant
 \item preemptable or non-preemptable
 \item periodic or aperiodic
\end{itemize}

\noindent(2) A task can have timing constraints
\begin{itemize}
 \item $b$ : release time
 \item $c$, $d$ : execution time and deadline
 \item $p$ : period for periodic task
 \item $p_1$, $p_2$: minimum and maximum inter-arrival times for aperiodic task
\end{itemize}


\noindent (3) A set of tasks can have `precedence constraints' \cite{TIMING}.

\noindent (4) A scheduling algorithm can be \\
\begin{tabular}{ll}
  Earliest Deadline First & $\pi \stackrel{def}{=} d_{max} - (d_i - t)$ \\
  Deadline Monotonic & $\pi \stackrel{def}{=} d_{max} - d_i$ \\
  Shortest Renaming Time First & $\pi \stackrel{def}{=} c_{max} - (c_i - s)$ \\
  Least Laxity First & $\pi \stackrel{def}{=} d_{max} - (d_i - t) - (c_i - s)$
\end{tabular}

\subsection{Periodic System Models}
A system model consists of a non-emptyset of infinite tasks which defined by basic ACSR. We consider the periodic task model $T(\Pi, \Theta)$, where $\Pi$ is a period and $\Theta$ is an execution time requirement($\Theta \leq \Pi$).

A basic demand process $P_{e,c}$ represeting the \textit{periodic}\cite{PERIODIC} task model $T(\Pi, \Theta)$ is defined as follows:
\[
\begin{array}{rcll}
  P_{e,c}&\stackrel{def}{=}&\emptyset:P_{e+1,c} + \{(cpu,\pi)\}:P_{e+1,c+1} & \Pi-e > \Theta-c \textrm{, } c < \Theta  \\
  P_{e,c}&\stackrel{def}{=}& \{(cpu,\pi)\}:P_{e+1,c+1} & \Pi-e = \Theta-c\textrm{, } c < \Theta   \\
  P_{e,c}&\stackrel{def}{=}&\emptyset:P_{e+1,c}  & e<\Pi\textrm{, } c=\Theta \\
  P_{e,c}&\stackrel{def}{=}& P_{0,0}& e=\Pi\textrm{, } c=\Theta\\
  \end{array} \]

$P_{0,0}$ executes with $cpu$ for \textit{exactly} $\Theta$ time units out of $\Pi$ time units. Intuitively, when it comes to $P_{e,c}$, $e$ is the elapsed time from the begining of the current period, and $c$ is the accumulated time that it has executed for so far in the current period.

Excution of a system model depends on posiblity of using $cpu$ and semantics of ACSR, especially priority concepts. It is clear that when no $cpu$ provided at a time $t$, every task should idle one time unit at the time. If, in each task, priorities of demaning $cpu$ are same , it is considered as fixed priority scheduling model. Having dynamic priority, we can model various scheduling algorithm by encoding priorities. We describe priorities for EDF and RM scheduling as follows.
%As a scheduling algorithm, we consider the earliest-deadline-first(EDF) algorhtm and the rate-monotonic (RM) algorithm.
%In ACSR approach, priorities of the resource $cup$ encodes a scheduling algorithm. In order to reflect the EDF and RM, we use the following expression as the priority in each process $P_{e,c}$.
\begin{center}
\begin{tabular}{ll}
  Earliest Deadline First & $\pi \stackrel{def}{=} \textrm{MAX} - (\Pi - e)$ \\
  Rate Monotonic & $\pi \stackrel{def}{=} \textrm{MAX} - \Pi$ \\
\end{tabular}
\end{center}

\begin{exmp}
$T(3,1)$ with fixed priority $1$ can be defined as follows.
\[
\begin{array}{rcl}
  P_{0,0}&\stackrel{def}{=}&\emptyset:P_{1,0} + \{(cpu,1)\}:P_{1,1} \\
  P_{1,0}&\stackrel{def}{=}&\emptyset:P_{2,0} + \{(cpu,1)\}:P_{2,1} \\
  P_{1,1}&\stackrel{def}{=}&\emptyset:P_{2,1} \\
  P_{2,0}&\stackrel{def}{=}&\{(cpu,1)\}:P_{3,1} \\
  P_{2,1}&\stackrel{def}{=}&\emptyset:P_{3,1} \\
  P_{3,1}&\stackrel{def}{=}& P_{0,0} \\
  \end{array} \]
\end{exmp}


\section{Modeling Resource Supply (ACSR+)}

We consider the single processor system, so we assume that there is one suppliable resource called $\overline{cpu}$. A supply action supplies either none or the resource $\overline{cpu}$ during one ``tick'' of time which drawn from domain $\mathcal{D}_S = \{ \emptyset, \{\overline{cpu}\}\}$ ranged over by $B$. As an example, the singleton supply action $\{\overline{cpu}\}$ denotes the supply of resource $cpu$. The supply action $\emptyset$ represents no resource supply for one time unit.

The following grammar describes the syntax of supply processes:
\begin{eqnarray}
 S&::=& B:S \textrm{ $|$ } S \oplus S \textrm{ $|$ } C \nonumber\\
 B&::=&\emptyset \textrm{ $|$ } \{\overline{cpu}\} \nonumber
\end{eqnarray}
$B:S$ supplies a set of resources $B$ at the first time unit, and proceeds to the process $S$. The Choice operator $S \oplus T$ represents nondeterminism in that either of the processes may be chosen to execute.
%$S \widehat{\parallel} T$ describes the concurrent composition of $S$ and $T$.

\subsection{Semantics}

We let $\mathcal{S}$ denote a set of all supply processes. A labeled transition system $\rightarrow \subseteq \mathcal{S} \times \mathcal{D}_S \times \mathcal{S}$ is defined as follows:

\begin{tabular}{llll}
Prefix &
 $\vcenter{
  \infer[]{B:S \xrightarrow{B} S}{}
 }$  &
Rec &
 $\vcenter {
 \infer[C\stackrel{def}{=}S]{C \xrightarrow{B} S'}{S \xrightarrow{B} S'}
 }$ \\
ChoiceL &
 $\vcenter {
 \infer[]{S \oplus T \xrightarrow{B} S'}{S \xrightarrow{B} S'}
 }$ &
 ChoiceR &
 $\vcenter {
 \infer[]{S \oplus T \xrightarrow{B} T'}{T \xrightarrow{B} T'}
 }$
%  \\
% Parallel &
%  $\vcenter {
%  \infer[]{S \widehat{\parallel} T \xrightarrow{B \cup B'} S' \widehat{\parallel} T'}{S \xrightarrow{B} S' & T \xrightarrow{B'} T' }
%  }$
\end{tabular}



%\subsection{Syntax of Supply Description Language}

%We let $\overline{\mathcal{R}} = \{ \bar{r} | r \in \mathcal{R} \}$ denote a finite set of suppliable resources. We say that $\bar{r}$ is its inverse resource; i.e. $\bar{\bar{r}} = r$. A supply action that supplies a set of resources during one ``tick''  of time is drawn from domain $\textbf{P}(\overline{\mathcal{R}})$. We use $\mathcal{D}_S$ to denote the domain of supply actions, and we let $\sigma$ range over $\mathcal{D}_S$. As an example, the singleton supply action $\{\bar{r}\}$ denotes the supply of some resource $r \in \overline{\mathcal{R}}$. The supply action $\emptyset$ represents no resource supply for one time unit. If a supply action $\sigma$ is $\{\overline{r_1}, \overline{r_2}\}$, then $\bar{\sigma} = \{r_1, r_2\}$

%The following grammar describes the syntax of supply processes:
%\begin{eqnarray}
%S &::=& \textrm{NIL} \textrm{ $|$ } \sigma:S \textrm{ $|$ } S \oplus S \textrm{ $|$ } C \nonumber
%\end{eqnarray}

%NIL is a supply process that executes no action (i.e. it is initially deadlocked). $\sigma$:$S$ supplies a set of resources $\sigma$ at the first time unit, and proceeds to the process $S$. The Choice operator $S \oplus T$ represents non-determinism in that either of the processes may be chosen to execute.

%We note that we don't have any parallel operator like $\parallel_S$ yet. We, currently, consider a single partition (or component).

%\subsection{Operational Semantics}

%We let $\mathcal{S}$ denote a set of all supply processes. A labeled transition system $\rightarrow \subseteq \mathcal{S} \times \mathcal{D}_S \times \mathcal{S}$ is defined as follows:

% \begin{figure}
% \centering
%\begin{tabular}{llllll}
%Prefix &
% $\vcenter{
%  \infer[]{\sigma.S \xrightarrow{\sigma} S}{}
% }$  &
%ChoiceL &
% $\vcenter {
% \infer[]{S \oplus T \xrightarrow{\sigma} S'}{S \xrightarrow{\sigma} S'}
% }$ &
%Rec &
% $\vcenter {
% \infer[C\stackrel{def}{=}S]{C \xrightarrow{\sigma} S'}{S \xrightarrow{\sigma} S'}
% }$ \\\\
%

%\end{tabular}
% \caption{Late Operational Semantics}
% \label{LATE}
% \end{figure}


\subsection{Specifying Resource Model}

Currently, we assume uniprocessor system with one suppliable resource called $cpu$. However, we believe that this framework can deal with multiple resources without any modification of the framework.

\begin{eqnarray}
 S_1 & \stackrel{def}{=} & \{\}:S_1 \nonumber \\
 S_2 & \stackrel{def}{=} & \{\overline{cpu}\}:S_2 \nonumber \\
 S_3 & \stackrel{def}{=} & \{\}:S_3 \oplus \{\overline{cpu}\}:S_3 \nonumber
\end{eqnarray}

$S_1$ is a supply process which never grant any resource. $S_2$ is a supply process which always grants $\overline{cpu}$. $S_3$ non-deterministically decide it is going to grant or not. In the view point of task demand, $S_3$ might behave like $S_1$ in the worst case, but $S_2$ in the best case.

% We consider following two resource models.
% \begin{itemize}
%  \item Periodic resource model
%  \item Explicit Deadline Periodic resource model
% \end{itemize}

A supply process $S_{e,c}$ represeting the \textit{periodic}\cite{PERIODIC} resource model $\Gamma(\Pi, \Theta)$ is defined as follows:

\[
\begin{array}{rcll}
  S_{e,c}&\stackrel{def}{=}&\emptyset:S_{e+1,c} \oplus \{\overline{cpu}\}:S_{e+1,c+1} & \Pi-e > \Theta-c \textrm{, } c < \Theta  \\
  S_{e,c}&\stackrel{def}{=}& \{\overline{cpu}\}:S_{e+1,c+1} & \Pi-e = \Theta-c\textrm{, } c < \Theta   \\
  S_{e,c}&\stackrel{def}{=}&\emptyset:S_{e+1,c}  & e<\Pi\textrm{, } c=\Theta \\
  S_{e,c}&\stackrel{def}{=}& S_{0,0}& e=\Pi\textrm{, } c=\Theta\\
  \end{array} \]

$S_{0,0}$ non-deterministically grants $cpu$ for \textit{exactly} $\Theta$ time units out of $\Pi$ time units.
Intuitively, when it comes to $S_{e,c}$, $e$ is the elapsed time from the begining of the current period, and $c$ is the accumulated time that it has granted for so far in the current period.
\begin{eqnarray}
 S_4 & \stackrel{def}{=} & \{\}:\{\overline{cpu}\}:S_4 \oplus \{\overline{cpu}\}:\{\}:S_4 \nonumber
\end{eqnarray}

If $\Pi = 2$ and $\Theta = 1$, we get $S_4$ as a periodic resource provider $\Gamma(2,1)$. $S_4$ exactly grants $cpu$ for 1 time units out of 2 time units.

\section{Compositional Schedulability Analysis}

\section{Supply Demand Relation}
Given a demand process $P$, we use $trace(P) = \{ A_1 A_2\cdots \in  {\mathcal{D}_R}^{\omega} \mid P \xrightarrow{A_1}_\pi \xrightarrow{A_2}_\pi  \cdots \}$ to denote a set of all infinite traces generated from $P$, ranged over by $tp \in {\mathcal{D}_R}^{\omega}$.
Given a supply process $S$, we use $trace(S) = \{ B_1 B_2\cdots \in  {\mathcal{D}_S}^{\omega} \mid S \xrightarrow{B_1} \xrightarrow{B_2}  \cdots \}$ to denote a set of all infinite traces generated from $S$, ranged over by $ts \in {\mathcal{D}_S}^{\omega}$. $tp_i$ and $ts_i$ denotes the $i$'th timed step of $tp$ and $ts$ respectively. We say $P \xrightarrow{A_1 A_2 \cdots A_n} P'$ for $\exists P_i, P \xrightarrow{A_1} P_1 \xrightarrow{A_2} \cdots \xrightarrow{A_{n-1}} P_{n-1} \xrightarrow{A_n} P'$.

\begin{defn}
The relation $\models \subseteq {\mathcal{D}_S}^{\omega} \times P$ is a binary relation, where the left side is a set of infinite traces of supply process and the right side is a demand process. $\models$ is called the \textit{supply demand relation}. We define it as follows:
\\

\begin{tabular}{lcl}
$t \models NIL$ & iff \textrm{ } & false \\
$\{\} \cdot t' \models P$ & iff \textrm{ } & $\exists P', P \xrightarrow{\emptyset}_\pi P'$ \\
  &     & $\forall P', P \xrightarrow{\emptyset}_\pi P' \implies t' \models P'$\\
$\{\overline{cpu}\} \cdot t' \models P$ & iff \textrm{ } & $\forall P', P \xrightarrow{\{(cpu,n)\}}_\pi P' \implies t' \models P'$, and \\
  &     & unless $P \xrightarrow{\{(cpu,n)\}}_\pi$, then $\forall P', P \xrightarrow{\emptyset}_\pi P' \implies t' \models P'$
\end{tabular}

We write $ S \models P$ for $ \forall t \in trace(S), t \models P.$
\end{defn}


% definition #2

\begin{defn}
The relation $\models \subseteq S \times P$ is a binary relation, where the left side is a  supply process and the right side is a demand process. We assume that $P$ is given as follows:
$$ P = \sum_{i=1}^{n} \{\}\colon\negthinspace Q_i + \sum_{j=1}^{m} \{(cpu,\pi)\}\colon\negthinspace R_j$$

$\models$ is called the \textit{supply demand relation}. We define it as follows:
\\

\begin{tabular}{lcl}
$\{\} : S_1 \models P$ & iff \textrm{ } & 
$n > 0$ and $\forall 1 \leq i \leq n, S_1 \models Q_i$ \\
$\{\overline{cpu}\} : S_1 \models P$ & iff \textrm{ } & 
if $m > 0$ then $\forall 1 \leq j \leq m, S_1 \models R_j$ \\
& & else $\forall 1 \leq i \leq n, S_1 \models Q_i$ \\

$\{\}:S_1 + \{\overline{cpu}\} : S_2 \models P$ & iff \textrm{ } & 
$n > 0$ and $\forall 1 \leq i \leq n, S_1 \models Q_i$, and\\

   &     & if $m > 0$ then $\forall 1 \leq j \leq m, S_1 \models R_j$

\end{tabular}


\end{defn}




%
%
%\subsection{Schedulable Under Relation}
%
%We assume a supply process $S$ itself contains no deadlock. We use $S \models P$ to denote $P$ is \textit{schedulable under} $S$. We say that $S \nvDash \textrm{NIL}$ for any $S$. This is because we will reduce \textit{schedulable under} relation checking problem into deadlock checking problem in ACSR. Therefore, we define the definition of \textit{schedulable under} relation considering the nature of deadlock in ACSR.
%
%To define the \textit{schedulable under} relation $\models$, we consider two cases. The first case (Def. 4.1) is that $P$ doesn't contain an instantaneous action at the first step. The second case (Def. 4.2) is that $P$ contains at least one instantaneous action at the first step. We combine two cases, and finally get Def. 4.3. The definitions are recursive, so we should avoid resursiveness later.
%
%\begin{defn}[Case 1: $\nexists P', P \xrightarrow{e} P'$] $S \models P$ if and only if
%\begin{enumerate}
% \item $\forall S' \mid S \xrightarrow{\sigma} S'$, $\exists P', [P]_{\bar{\sigma}} \xrightarrow{A}_\pi [P']_{\bar{\sigma}}$ where $\rho(A) \subseteq \bar{\sigma}$
% \item $\forall S' \mid S \xrightarrow{\sigma} S'$, $\forall P' \mid [P]_{\bar{\sigma}} \xrightarrow{A}_\pi [P']_{\bar{\sigma}}$ where $\rho(A) \subseteq \bar{\sigma}$, $S' \models P'$
%\end{enumerate}
%\end{defn}
%
%Let's consider the following processes that contain no event at the first step.
%\begin{eqnarray}
% P_1 & \stackrel{def}{=} & \{(cpu,1)\}:P_1 \nonumber \\
% P_2 & \stackrel{def}{=} & \{\}:P_2 + \{(cpu, 1)\}:P_2 \nonumber \\
% P_3 & \stackrel{def}{=} & \{\}:\textrm{NIL} + \{(cpu,1)\}:P_3 \nonumber \\
% P_4 & \stackrel{def}{=} & \{\}:(\{\}:\textrm{NIL} + \{(cpu,1)\}:P_4) + \{(cpu,1)\}:\{\}:P_4 \nonumber
%\end{eqnarray}
%
%Obviously, $S_2 \models P_1$. $P_2$ and $P_3$, respectively, are schedulable under $S_2$. Whenever $S_2$ grants $\overline{cpu}$, $P_2$ and $P_3$ always use it because $[P_2]_{\{cpu\}} \xrightarrow{\{(cpu,1)\}}_\pi [P_2]_{\{cpu\}}$ and $[P_3]_{\{cpu\}} \xrightarrow{\{(cpu,1)\}}_\pi [P_3]_{\{cpu\}}$ are an unique transition of $[P_2]_{\{cpu\}}$ and $[P_3]_{\{cpu\}}$ respectively. $P_4$ represents a preemptable periodic task $T(2,1)$ which demands $cpu$ for 1 time unit out of every 2 time units and goes to NIL if it misses its deadline. We note that $S_4 \models P_4$ according to the definition, which denotes $T(2,1)$ is schedulable under $\Gamma(2,1)$.
%
%
%\begin{defn}[Case 2: $\exists P', P \xrightarrow{e} P'$] $S \models P$ if and only if
%\begin{enumerate}
% \item $\forall P' \mid P \xrightarrow{e}_{\pi} P'$, $S \models P'$
% \item $\forall S' \mid S \xrightarrow{\sigma} S'$, $\forall P' \mid [P]_{\bar{\sigma}} \xrightarrow{A}_\pi [P']_{\bar{\sigma}}$ where $\rho(A) \subseteq \bar{\sigma}$, $S' \models P'$
%\end{enumerate}
%\end{defn}
%
%Let's consider the following processes that contain an event at the first step.
%\begin{eqnarray}
% P_5 & \stackrel{def}{=} & \{\}:\textrm{NIL} + \{(cpu,1)\}:\textrm{NIL} + (\tau,1).\{\}:P_5 \nonumber \\
% P_6 & \stackrel{def}{=} & \{(cpu,1)\}:\textrm{NIL} + (\tau,0).\{\}:P_6 \nonumber \\
% P_7 & \stackrel{def}{=} & \{\}:\textrm{NIL} + (\tau,0).\{\}:P_7 \nonumber \\
% P_8 & \stackrel{def}{=} & \{\}:P_8 + (\tau,0).\textrm{NIL} \nonumber
%\end{eqnarray}
%
%$S_1 \models P_5$ because $[P_5]_{\{cpu\}} \xrightarrow{(\tau,1)}_\pi [P_5]_{\{cpu\}}$ is an unique transition of $[P_5]_{\{cpu\}}$ and $S_1 \models \{\}:P_5$. $S_2 \models P_6$ because the transition $[P_6]_{\{cpu\}} \xrightarrow{\{(cpu,1)\}}_\pi [P_6]_{\{cpu\}}$ can't be enabled unless $S_1$ grants $\overline{cpu}$, and $S_1$ does not. $S_1 \nvDash P_7$ because the transition $[P_7]_{\{cpu\}} \xrightarrow{\{\}}_\pi [\textrm{NIL}]_{\{cpu\}}$ can be taken and $S_1 \nvDash \textrm{NIL}$. In the same way, $S_1 \nvDash P_8$ because the transition $[P_8]_{\{cpu\}} \xrightarrow{(\tau,0)}_\pi [\textrm{NIL}]_{\{cpu\}}$ can be taken and $S_1 \nvDash \textrm{NIL}$.
%
%We simply combine the definition 4.1 and definition 4.2.
%Finally, we get:
%\begin{defn} $S \models P$ if and only if
%\begin{enumerate}
% \item if $\nexists P', P \xrightarrow{e} P'$, then $\forall S' \mid S \xrightarrow{\sigma} S'$, $\exists P', [P]_{\bar{\sigma}} \xrightarrow{A}_\pi [P']_{\bar{\sigma}}$ where $\rho(A) \subseteq \bar{\sigma}$
% \item $\forall P' \mid P \xrightarrow{e}_{\pi} P'$, $S \models P'$
% \item $\forall S' \mid S \xrightarrow{\sigma} S'$, $\forall P' \mid [P]_{\bar{\sigma}} \xrightarrow{A}_\pi [P']_{\bar{\sigma}}$ where $\rho(A) \subseteq \bar{\sigma}$, $S' \models P'$
%\end{enumerate}
%\end{defn}

\subsection{Reducing to Bisimulation Checking in ACSR}

We say $\overline{S}$ is its inverse. The goal of this subsection is to define translation (or inversion) rules so that we can make the following propositions true.

\begin{prop}
$S \models P$ if and only if $[P \parallel \overline{S}]_\mathcal{R} \backslash \backslash \mathcal{R} \simeq_\pi \emptyset^\infty$
\end{prop}

\begin{prop}
$S \models P$ if and only if $[P \parallel \overline{S}]_\mathcal{R}$ is a non-Zeno process and deadlock-free.
\end{prop}


\begin{prop}
$S \models P$ if and only if $[P \parallel \overline{S}]_\mathcal{R}$ is deadlock-free.
\end{prop}


The translation (or inversion) rules are as follows:

\begin{tabular}{ll}
$S$ & $\overline{S}$ \\ \hline
$\sigma:S$ & $\{(r,\infty)|\bar{r} \in \overline{\mathcal{R}} \setminus \sigma\}:\overline{S}$ \\
$S \oplus T$ & $(\tau,\infty).\overline{S} + (\tau,\infty).\overline{T}$ \\
$C$ & $\overline{C}$ \\
NIL & NIL \\
\end{tabular}

\begin{tabular}{ll}
$S$ & $\overline{S}$ \\ \hline
$\{\overline{cpu}\}:S$ & $\{\}:\overline{S}$ \\
$\{\}:S$ & $\{(cpu,\infty)\}:\overline{S}$ \\
$S \oplus T$ & $(\tau,\infty).\overline{S} + (\tau,\infty).\overline{T}$ \\
$C$ & $\overline{C}$ \\
NIL & NIL \\
\end{tabular}



Furthermore, each definition $C \stackrel{def}{=} S$ is translated into $\overline{C} \stackrel{def}{=} \overline{S}$.

We assume $\mathcal{R} = \{cpu\}$. Let's consider the examples as follows:
\begin{eqnarray}
 \overline{S_1} & \stackrel{def}{=} & \{(cpu,\infty)\}:\overline{S_1} \nonumber \\
 \overline{S_2} & \stackrel{def}{=} & \{\}:\overline{S_2} \nonumber \\
 \overline{S_3} & \stackrel{def}{=} & (\tau,\infty).\{(cpu,\infty)\}:\overline{S_3} + (\tau,\infty).\{\}:\overline{S_3} \nonumber \\
 \overline{S_4} & \stackrel{def}{=} & (\tau,\infty).\{(cpu,\infty)\}:\{\}:\overline{S_4} + (\tau,\infty).\{\}:\{(cpu,\infty)\}:\overline{S_4} \nonumber
\end{eqnarray}

We note that $\overline{S_i}$ are ordinary ACSR processes. $S_1$ doesn't grant any resource at the first time unit, so $\overline{S_1}$ does an action $\{(cpu,\infty)\}$ at the first time unit so that any other process, running in parallel, can't use $cpu$. $S_2$ grants $\overline{cpu}$ at the first time unit, so $\overline{S_2}$ does an action $\{\}$ at the first time unit so that another process, running in parallel, can use $cpu$. $S_3$ non-deterministicallly chooses an action between $\{\}$ and $\{\overline{cpu}\}$, so we add dummy events $(\tau, \infty)$ into $\overline{S_3}$ in order to preserve the non-determinism. We note that $[P_4 \parallel \overline{S_4}]_{\{cpu\}} \backslash \backslash \{cpu\}$ is weakly bisimular to $\emptyset^\infty$. We'd like this to mean that $T(2,1)$ is schedulable under $\Gamma(2,1)$

\section{Interface Generation}

For a component $C(W,A)$, the interface generation problem is to generate an optimal interface $I$.
\subsection{Periodic Model}
We assume the resource model is periodic. For a component $C(W,A)$, the interface generation problem is to generate an optimal periodic interface $\mathcal{P}(P,E)$. Given a component $C$ and a period of interface $P_0$, the optimal interface is $P(P_0, E_0)$ with the minimum $E_0$ such that $P$ of $C$ is schedulable. In the algorithm, we assume that $C(W,A)$is schedulable under the full resource supply.

\begin{algo} Here is an abstract algorithm.
\begin{verbatim}
Input : C(W,A), P
Output: E

for e := 1 to P
  R = periodic resource model (P,e)
  if (S(W,R,A) is schedulable) then
    return e
\end{verbatim}
\end{algo}

\begin{algo}
We refine the algorithm above as follows:
\begin{verbatim}
Input : C(W,A), P
Output: E

T = encode C(W,A) as an ACSR process
for e := 1 to P
  R = periodic resource model (P,e)
  S = encode R as a supply process
  if ([T||Inv(S)]_{cpu}\\{cpu} is bisimular to Idle) then
    return e
\end{verbatim}
\end{algo}


\begin{algo}
We refine the algorithm above as follows:
\begin{verbatim}
Input : C(W,A), P
Output: E

T = encode C(W,A) as an ACSR process
for e := 1 to P
  R = periodic resource model (P,e)
  S = encode R as a supply process
  if ([T||Inv(S)]_{cpu} is deadlock-free) then
    return e
\end{verbatim}
\end{algo}


%\subsection{Explicit Deadline Periodic Model}

\section{Experimental Results}

We implemented the algorithm in python script language and using VERSA. We compare the result to CARTS's. The workload model consists of periodic tasks $T(5,1)$ and $T(7,1)$. The scheduling algorithm is EDF.

The table below shows the optimal periodic interface for a given period $P$. We round up(ceiling) the CARTS's real number results to be comparable with ACSR/VERSA's.

\begin{center}
\begin{tabular}{ccc}
P & E(CARTS) & E(ACSR/VERSA)\\
1 & 1 & 1\\
2 & 1 & 1\\
3 & 2 & 2\\
4 & 2 & 2\\
5 & 3 & 3\\
6 & 4 & 4\\
7 & 5 & 5\\
8 & 6 & 6\\
9 & 7 & 7\\
10 & 8 & 8\\
11 & 9 & 9
\end{tabular}
\end{center}

\section{Conclusion}

This paper describes a process algebraic framework for reasoning about resource demand and supply. We demonstrated a framework of schedulability analysis and periodic interface generation for a single scheduling unit(, partition or component) with a single shared resource.

As an illustration, we use VERSA, a tool kit for ACSR, to check of truth of supply-demand relation and compositional schedulability analysis.

We will extend this framework to partition(component) composition with composition of supply processes.

% \begin{tabular}{ll}
% Close &
%  $\vcenter{
%   \infer[A_2 = f_I(A_1)]{[P]_I \xrightarrow{A_2} [P']_I}{P \xrightarrow{A_1} P' & \nexists r, r? \in A_1 \wedge r! \notin A_1}
%  }$  \\
% \end{tabular}
% \begin{eqnarray}
% f_I(A)&=&\{(r,n+m) \mid (r!,n),(r?,m) \in A\} \nonumber\\
%     &\cup& \{(r,n) \mid (r!,n) \in A, (r?,m) \notin A\} \nonumber \\
%     &\cup& \{(r,0) \mid (r!,n) \notin A, (r,m) \notin A, r \in I\} \nonumber
% \end{eqnarray}

\bibliographystyle{plain}
\bibliography{ref}

\end{document}
